\documentclass{llncs}

\usepackage{url}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}


\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}

\newcommand{\text}[1]{\mbox{#1}}
\newcommand{\wc}{\_}
\newcommand{\mulstep}{ \stackrel{*}{\leadsto}}
\newcommand{\lam}[2]{\lambda #1 . #2}
\newcommand{\evals}[2]{#1 \downarrow #2}

\newcommand{\wm}[0]{\stackrel{\textit{w}}{\to}}
\newcommand{\interp}[1]{[\negthinspace[#1]\negthinspace]}
\newcommand{\symm}[1]{\langle\textit{#1}\rangle}
\newcommand{\rrl}[1]{\textit{r-#1}}
\newcommand{\rrlb}[0]{\textit{r-}\beta}
\newcommand{\trl}[1]{\textit{t-#1}}
\begin{document}
%\pagestyle{empty}
\title{ Version V}
\author{Peng Fu}
\institute{Computer Science, The University of Iowa}
\date{March 7, 2012}


\maketitle
\thispagestyle{empty}


\section{System F}

\subsection{Syntax}


\noindent $\mathbf{Types} \ T \ ::= \ X  \ |  \ \Pi x:T_1. T_2 \ | \ \forall X.T$

\

\noindent $\mathbf{Terms} \ t \ ::= \ x \ | \ (t_1 \ t_2) \ | \ \lambda x.t$

\

\noindent \textbf{Reduction Contexts} 

\

$C \ ::= * \ | \ C \ t \ | \ \lambda x.C \ | \ t \ C$

\

\noindent $\mathbf{Values} \ v \ ::= \lambda x.t$

\

\noindent \textbf{Reductions} 

\

\noindent Full Beta Reduction.

\

$C[(\lambda x.t) \ t'] \leadsto C[[t'/x]t]$

\subsection{Typing Context}

\noindent $\mathbf{Context} \ \Gamma ::=\cdot \ | \ \Gamma, x:T \ | \ \Gamma , X$

\

\begin{definition}
\noindent We define $FV(\Gamma)$ inductively:

\

\noindent $FV(\cdot) = \emptyset$.

\

\noindent $FV(\Gamma,x:T)= FV(\Gamma)$.

\

\noindent $FV(\Gamma, X) = \{X\} \cup FV(\Gamma)$.
\end{definition}

\begin{definition}
\noindent We define $FVar(\Gamma)$ inductively:

\

\noindent $FVar(\cdot) = \emptyset$.

\

\noindent $FVar(\Gamma,x:T)= FVar(\Gamma) \cup \{x\}$.

\

\noindent $FVar(\Gamma, X) = FVar(\Gamma)$.
\end{definition}

\begin{definition}[Well-formness]

\

\infer{\cdot \vdash \mathbf{OK}}{}

\

\infer{\Gamma, X \vdash \mathbf{OK}}{\Gamma \vdash \mathbf{OK}}

\

\infer{\Gamma, x:T \vdash \mathbf{OK}}{\Gamma \vdash \mathbf{OK} && FV(T) \subseteq FV(\Gamma)}

\end{definition}

\noindent We will assume well-formness of the context from now on.

\subsection{Typing}

\

\infer[{\textit{T\_Var}}]{\Gamma\vdash x : T }{(x:T) \in \Gamma } 

\ 

\infer[{\textit{$\to$\_intro}}]{\Gamma\vdash \lam{x}{t} : \Pi x:T_1. T_2}
      {\Gamma,x:T_1 \  \vdash t:T_2}

\

\infer[{\textit{$\to$\_elim}}]{\Gamma\vdash t_1\ t_2 : T_2}
      {\Gamma\vdash t_1 : \Pi x:T_1. T_2 \  &
       \Gamma\vdash t_2 : T_1 }
       
\

\infer[{\textit{$\forall$\_intro}}]{\Gamma \vdash t:\forall X.T}{\Gamma,X \vdash t:T }

\

\infer[{\textit{$\forall$\_elim}}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t:\forall X.T && FV(T') \subseteq FV(\Gamma)}

 
\section{Rewriting Simulation}

\subsection{Syntax}

\noindent $\mathbf{Types} \ T \ ::= \ X  \ |  \ \Pi x:T_1. T_2 \ | \ \forall X.T$

\

\noindent $\mathbf{Terms} \ t \ ::= \ x \ | \ (t_1 \ t_2) \ | \ \lambda x.t$

\

\noindent $\mathbf{Typing \ Context}\  \Gamma \ ::= \cdot \ | \ \Gamma, x:T \ | \ \Gamma,X$.

\

\noindent $\mathbf{PreTypes} \ P \ ::=  \Gamma x \ | \  \Gamma X\ | \ \Pi x:T. P' \ | \ P_1 P_2 \ |\ 
 \lambda x. P \ | \ \forall X.P $

\

\noindent $\mathbf{RedContext} \ E \ ::= \ []\ | \ E \ P \ | \ P \ E \ | \ \lambda x.E \ | \  \forall X.E \ | \ \Pi x:T.E $

   
\begin{definition}

\noindent We define $FV (P)$ inductively:

\

\noindent $FV (\Gamma x) = FV(\Gamma)$.

\

\noindent $FV (\Gamma X) = \{X\} \cup FV(\Gamma)$.

\

\noindent $ FV (P_1 P_2)= FV(P_2) \cup FV(P_1)$

\

\noindent $FV (\Pi x:T. P)= FV(T) \cup FV(P)$

\

\noindent $FV (\lambda x. P)= FV (P)$

\
 
\noindent $FV (\forall X.P)= FV (P) - \{X \}$

\end{definition}

\noindent Notice: $FV(T)$ is defined as usual.

\begin{definition}

\noindent We define $FVar (P)$ inductively:

\

\noindent $FVar (\Gamma x) = FVar(\Gamma) \cup \{x\}$.

\

\noindent $FVar (\Gamma X) = FVar(\Gamma)$.

\

\noindent $ FVar (P_1 P_2)= FVar(P_2) \cup FVar(P_1)$

\

\noindent $FVar (\Pi x:T. P)=  FVar(P) - \{x\}$

\

\noindent $FVar (\lambda x. P)= FVar (P) - \{x\}$

\
 
\noindent $FVar (\forall X.P)= FVar (P) $

\end{definition}

\begin{definition}

\noindent We can extend the constructions of $\Gamma x$ and $\Gamma X$ to arbitrary
terms and types as following.

\

\noindent $\Gamma (t_1 t_2) \equiv (\Gamma t_1)( \Gamma t_2) $.

\

\noindent $\Gamma (\lambda x.t) \equiv \lambda x. (\Gamma t)$.

\

\noindent $\Gamma (\Pi x:T_1. T_2) \equiv  \Pi x:T_1 .( [\Gamma,x:T_1] T_2) $. 

\ 

\noindent $\Gamma (\forall X.T) \equiv \forall X. ([\Gamma,X ]T)$.

\

\end{definition}

\noindent Notice: $\Gamma t \in \mathbf{PreTypes}$ and $\Gamma T \in \mathbf{PreTypes}$ by the definition above.



\begin{definition}[Global Context]

\noindent We define the global context of a pretype $P$, namely $\mathcal{G}(P)$ inductively: 

\

\noindent $\mathcal{G}(\Gamma x) = \Gamma$.

\
 
\noindent $\mathcal{G}(\Gamma X) = \Gamma$.

\

\noindent $\mathcal{G}(\Pi x:T'.P) = \mathcal{G}(P)- [x:T']$

\

\noindent $\mathcal{G}(P_1 P_2) = \mathcal{G}(P_1)\cup \mathcal{G}(P_2)$

\

\noindent $\mathcal{G}(\lambda x.P) = \mathcal{G}(P)$

\

\noindent $\mathcal{G}(\forall Y.P) = \mathcal{G}(P) $. 

\end{definition}


\subsection{Syntactical Definitions}

\noindent From now on, we will assume modulo renaming up to alpha equivalence. And we will assume capture avoiding for substitution.



\begin{definition}
Define a new operation $[x:T] \cdot P$ inductively on the structure of $P$:

\

\noindent $[x:T] \cdot \Gamma y\equiv [\Gamma,x:T]y$. 

\

\noindent $[x:T] \cdot\Gamma Y\equiv [\Gamma,x:T] Y$. 

\

\noindent $[x:T] \cdot (P_1 P_2) \equiv ([x:T] \cdot P_1)([x:T] \cdot P_2)$

\

\noindent $[x:T] \cdot (\Pi y:T'. P) \equiv  \Pi y:T' .([x:T] \cdot P)$

\

\noindent $[x:T] \cdot \lambda y.P \equiv \lambda y.([x:T] \cdot P)$. 

\

\noindent $[x:T] \cdot \forall X.P \equiv \forall X.([x:T] \cdot P) $.


\end{definition}

\begin{definition}
Define a new operation $[X] \cdot P$ inductively on the structure of $P$:

\

\noindent $[X] \cdot \Gamma y\equiv [\Gamma,X]y$. 

\

\noindent $[X] \cdot\Gamma Y\equiv [\Gamma,X] Y$. 

\

\noindent $[X] \cdot (P_1 P_2) \equiv ([X] \cdot P_1)([X] \cdot P_2)$

\

\noindent $[X] \cdot (\Pi x:T'. P) \equiv  \Pi x:T' .([X] \cdot P)$

\

\noindent $[X] \cdot \lambda y.P \equiv \lambda y.([X] \cdot P)$. 

\

\noindent $[X] \cdot \forall Y.P \equiv \forall Y.([X] \cdot P) $.


\end{definition}


\subsection{ Reductions}

\noindent $E[ (\lambda x. P)] \leadsto_\lambda E[\Pi x:T. [x:T]\cdot P]$, where $FV(T) \subseteq FV(\mathcal{G}(P))$. 

\

\noindent $E[( \Pi x:T. [\Gamma,x:T]T')\Gamma T] \leadsto_\epsilon E[\Gamma T']$.

\

\noindent $E[P] \leadsto_\pi E[ \forall X.[X]\cdot P]$, where  $X \notin FV(\mathcal{G}(P))$. 

\

\noindent $E[\forall X.[\Gamma,X]T] \leadsto_\iota E[\Gamma [S/X]T]$, where $FV(S)\subseteq FV(\Gamma)$.

\

\noindent $E[ \Gamma x] \leadsto_s E[\Gamma T]$, where $(x:T) \in \Gamma$.

\

\noindent Notice: we use $\leadsto$ as a shorthand for $\leadsto_\lambda \cup \leadsto_\epsilon \cup \leadsto_\pi \cup \leadsto_\iota  \cup \leadsto_s$. 

\

\noindent We can go ahead and define $\mulstep$:

\

\infer[\textit{ref}]{ P \mulstep P}{}

\

\infer[\textit{trans}]{P \mulstep P'}{P \mulstep P'' & P'' \mulstep P'}

\

\noindent Notations: we use $\forall X^n.P$ as a shorthand for $\forall X_{n}.\forall X_{n-1}...\forall X_1. P$ and $\forall X^0.P \equiv P$.

\section{Soundness}

\begin{theorem}
\noindent If $\Gamma \vdash t:T$, then $\Gamma t \mulstep \Gamma T$.

\end{theorem}

\begin{proof}
\noindent By induction on the derivation of $\Gamma \vdash t:T$.

\

\noindent Base Case: 

\

\infer[{\textit{T\_Var}}]{\Gamma\vdash x : T }{(x:T) \in \Gamma } 

\

\noindent We know that $\Gamma x \leadsto_s \Gamma T $, where $(x:T) \in \Gamma$. So it is the case. 

\

\noindent Step Case:

\

\infer[{\textit{$\to$\_intro}}]{\Gamma\vdash \lam{x}{t} : T_1 \to T_2}
      {\Gamma,x:T_1 \  \vdash t:T_2}

\

\noindent We have $\Gamma (\lambda x.t) \equiv \lambda x.\Gamma t \leadsto_\lambda  T_1 \to [\Gamma,x:T_1]t$. By IH, we know that $[\Gamma,x:T_1]t \mulstep [\Gamma,x:T_1]T_2$. By congruence, we know that $\Gamma (\lambda x.t) \equiv \lambda x.\Gamma t \mulstep  T_1 \to [\Gamma,x:T_1]t \mulstep T_1 \to [\Gamma,x:T_1]T_2 \equiv \Gamma (T_1 \to T_2)$.

\

\noindent Step Case:

\

\infer[{\textit{$\to$\_elim}}]{\Gamma\vdash t_1\ t_2 : T_2}
      {\Gamma\vdash t_1 : T_1 \to T_2 \  &
       \Gamma\vdash t_2 : T_1 }
       
\

\noindent By IH, we know that $\Gamma t_1 \mulstep \Gamma (T_1 \to T_2) \equiv T_1 \to [\Gamma, x:T_1]T_2$ and $\Gamma t_2 \mulstep \Gamma T_1$. Thus we have $\Gamma t_1 t_2 \equiv (\Gamma t_1)(\Gamma t_2) \mulstep( T_1 \to [\Gamma,x:T_1]T_2)\Gamma T_1 \leadsto_\epsilon \Gamma T_2$.

\

\noindent Step Case:

\

\infer[{\textit{$\forall$\_intro}}]{\Gamma \vdash t:\forall X.T}{\Gamma \vdash t:T & X \notin FV(\Gamma)}

\

\noindent By IH, we know that $\Gamma t \mulstep \Gamma T$. Thus we have $\Gamma t \mulstep \Gamma T \leadsto_\pi \forall X.(\Gamma T) \equiv \Gamma (\forall X.T) $, where $X \notin FV(\Gamma)$.

\

\noindent Step Case:

\

\infer[{\textit{$\forall$\_elim}}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t:\forall X.T}

\

\noindent By IH, we have $\Gamma t \mulstep \forall X.\Gamma T \leadsto_\iota [T'/X]\cdot(\Gamma T) \equiv \Gamma ([T'/X]T)$. Thus it is the case.

\end{proof}

\section{Completeness}

\begin{lemma}
\label{appin}
\noindent If $\forall X^n.P_1 P_2 \mulstep \Gamma T$, then $\forall X^n. (P_1 P_2) \mulstep \forall Y^n.(T_1 \to [\Gamma,x:T_1]T_2)\Gamma T_1 \leadsto_\epsilon \forall Y^n.\Gamma T_2 \mulstep \Gamma T$ and we also have $\forall X^n.P_1 \mulstep T_1 \to [\Gamma,x:T_1]T_2$, $\forall X^n.P_2 \mulstep \Gamma T_1$. 

\end{lemma}

\begin{proof}
\noindent By induction on the length of $\forall X^n. P_1 P_2 \mulstep \Gamma T$.

\

\noindent Base Case: Impossible to arise.

\

\noindent Step Case: $\forall X^n.P_1 P_2 \leadsto P_3 \mulstep \Gamma T$. Case Split on $\leadsto$:

\

\noindent If $P_1 \equiv T_1 \to [\Gamma,x:T_1]T_2$ and $P_2 \equiv \Gamma T_1$, then $\forall X^n.P_1 P_2 \equiv \forall X^n.(T_1 \to [\Gamma,x:T_1]T_2)\Gamma T_1 \leadsto_\epsilon \forall X^n.\Gamma T_2 \mulstep \Gamma T$. Also $\forall X^n.P_1 \mulstep_\iota (T_1 \to [\Gamma,x:T_1]T_2) $ and $\forall X^n.P_2 \mulstep_\iota \Gamma T_1$. Thus it is the case.

\

\noindent If $\forall X^n.P_1 P_2 \leadsto_\pi \forall X^{n+1}. P_1 P_2 \mulstep \Gamma T$. By IH, $\forall X^{n+1}. P_1 P_2 \mulstep \forall Y^m.(T_1 \to [\Gamma,x:T_1]T_2)\Gamma T_1 \leadsto_\epsilon \forall Y^m.\Gamma T_2  \mulstep \Gamma T$ ,$\forall X^n. P_1 \leadsto_\pi \forall X^{n+1}.P_1 \mulstep T_1 \to [\Gamma,x:T_1]T_2$ and $\forall X^n.P_2 \leadsto_\pi \forall X^{n+1}.P_2 \mulstep \Gamma T_1$. So it is the case.

\

\noindent If $\forall X^n.P_1 P_2 \leadsto_\iota \forall X^{n-1}.[U/X_n]\circ ( P_1 P_2) \mulstep \Gamma T$. By IH, we have $ \forall X^{n-1}.[U/X_n]\circ ( P_1 P_2) \mulstep  \forall Y^m.(T_1 \to [\Gamma,x:T_1]T_2)\Gamma T_1 \leadsto_\epsilon \forall Y^m.\Gamma T_2  \mulstep \Gamma T$, $\forall X^n.P_1 \leadsto_\iota \forall X^{n-1}.[U/X_n]\circ P_1 \mulstep T_1 \to [\Gamma,x:T_1]T_2$ and $\forall X^n.P_2 \leadsto_\iota \forall X^{n-1}.[U/X_n]\circ P_2 \mulstep \Gamma T_1$. 

\

\noindent If $\forall X^n.P_1 P_2 \leadsto \forall X^n P_1' P_2 \mulstep \Gamma T$, where $P_1 \leadsto P_1'$. By IH, we have $ \forall X^n P_1' P_2 \mulstep \forall Y^m.(T_1 \to [\Gamma,x:T_1]T_2)\Gamma T_1 \leadsto_\epsilon \forall Y^m.\Gamma T_2  \mulstep \Gamma T$, $\forall X^n.P_1' \mulstep T_1 \to [\Gamma,x:T_1]T_2 $ and $ \forall X^n.P_2 \mulstep \Gamma T_1$. Thus $\forall X^n.P_1 \leadsto \forall X^n.P_1' \mulstep T_1 \to [\Gamma,x:T_1]T_2 $. So it is the case.



\end{proof}


\begin{lemma}
\label{absin}
\noindent If  $ \forall X^n.(\lambda x.P) \mulstep \Gamma T$, then $\forall X^n.\lambda x.P \mulstep   \forall Y^m.\lambda x.P' \leadsto_\lambda \forall Y^m.(T_1 \to [x:T_1]\cdot P') \mulstep \Gamma T$ and $\forall X^n .P \mulstep P'$. 
\end{lemma}
\begin{proof}
\noindent By induction on the length of $ \forall X^n.(\lambda x.P) \mulstep \Gamma T$.

\

\noindent Base Case: It is impossible to arise.

\

\noindent Step Case: $\forall X^n.(\lambda x.P) \leadsto P' \mulstep \Gamma T$. Case split on 
the first step $\leadsto$.

\

\noindent If $\forall X^n.(\lambda x.P) \leadsto_\lambda \forall X^n.(T_1 \to [x:T_1]\cdot P) \mulstep \Gamma T$. So it is the case. In this case, $\forall X^n.P \mulstep_\iota P$.

\

\noindent If $\forall X^n.\lambda x.P \leadsto_\pi \forall X^{n+1}. \lambda x.P \mulstep \Gamma T$. By IH, we have $ \forall X^{n+1}. \lambda x.P \mulstep    \forall Y^m.\lambda x.P' \leadsto_\lambda \forall Y^m.(T_1 \to [x:T_1]\cdot P')\mulstep \Gamma T$ and $ \forall X^{n+1}. P \mulstep P'$. Thus we have $\forall X^n.P \leadsto_\pi \forall X^{n+1}. P \mulstep P'$.


\

 \noindent If $\forall X^n.\lambda x.P \leadsto_\iota \forall X^{n-1}. \lambda x.[U/X_n]\circ P \mulstep \Gamma T$. By IH, we have $ \forall X^{n-1}. \lambda x.[U/X_n]\circ P \mulstep \forall Y^m.\lambda x.P'  \leadsto_\lambda \forall Y^m.(T_1 \to [x:T_1]\cdot P')\mulstep \Gamma T$ and $\forall X^{n-1}. [U/X_n]\circ P \mulstep P'$. Thus we have $\forall X^n.P \leadsto_\iota \forall X^{n-1}. [U/X_n]\circ P \mulstep P'$.

\

 \noindent If $\forall X^n.\lambda x.P \leadsto \forall X^n.\lambda x.P'' \mulstep \Gamma T$, where $P \leadsto P''$. By IH we have $ \forall X^n.\lambda x.P'' \mulstep \forall Y^m.\lambda x.P' \leadsto_\lambda \forall Y^m.(T_1 \to [x:T_1]\cdot P')\mulstep \Gamma T$ and $\forall X^n.P'' \mulstep P'$. Thus $\forall X^n. P \leadsto \forall X^n. P'' \mulstep P'$.


\end{proof}


\begin{lemma}
\label{arrow}
\noindent If $\forall X^n.(T \to P) \mulstep \Gamma T'$, then  $T' \equiv \forall Y^m.(T_1 \to T_2)$, $\delta T \equiv T_1$, $\delta \cdot P \mulstep [\Gamma,x:T_1]T_2$ for some type level substitution $\delta$.
\end{lemma}
\begin{proof}

\noindent By induction on the length of $\forall X^n.(T \to P) \mulstep \Gamma T'$.

\

\noindent Base Case: $\forall X^n.(T \to P)\equiv \Gamma T'$. In this case, $T \equiv T_1, T' \equiv \forall X^n.(T_1 \to T_2)$ and $P \equiv [\Gamma,x:T_1] T_2$ and $\delta = \emptyset$.  

\

\noindent Step Case: $\forall X^n.(T \to P) \leadsto P' \mulstep \Gamma T'$. Case split on the first step.

\

\noindent If $\forall X^n.(T \to P) \leadsto_\pi \forall X^{n+1}.(T \to P) \mulstep \Gamma T'$. By IH, $T' \equiv \forall Y^m.(T_1 \to T_2)$ and $\delta T \equiv T_1, \delta \cdot P \mulstep [\Gamma,x:T_1]T_2$. So it is the case.

\

\noindent If $\forall X^n.(T \to P) \leadsto_\iota \forall X^{n-1}.([U/X_n]T \to [U/X_n]\circ P) \mulstep \Gamma T'$. By IH, we have $\delta([U/X_n]T) \equiv [\delta U/X_n]\delta T \equiv T_1$ and $\delta \cdot ([ U/X_n]\circ P)\equiv [\delta U/X_n]\delta \cdot P \mulstep [\Gamma,x:T_1]T_2$. So it is the case.  

\

\noindent If $\forall X^n.(T \to P) \leadsto \forall X^n.(T \to P'') \mulstep \Gamma T'$, where $P \leadsto P''$. By IH, we have $\delta T \equiv T_1$ and $ \delta \cdot P'' \mulstep [\Gamma,x:T_1]T_2$. So $ \delta \cdot P \mulstep \delta \cdot P'' \mulstep [\Gamma,x:T_1]T_2$ by compatible with substitution. Thus it is the case. 

\end{proof}

\noindent Notice: Here we can see that we can actually construct the $\delta$ from the proof and $dom(\delta) \cap FV(\Gamma) = \emptyset$.

\begin{lemma}
\noindent If $P \leadsto P'$, then $\delta \cdot P \leadsto \delta \cdot P'$.

\end{lemma}

\begin{proof}
\noindent By induction on the derivation of $P \leadsto P'$.

\

\noindent Case: 

\

\infer{\lambda x.P \leadsto_\lambda T \to [x:T]\cdot P'}{}

\

\noindent We have $ \lambda x.\delta \cdot P \leadsto_\lambda \delta T \to [x:\delta \cdot T]\cdot (\delta \cdot P) \equiv \delta \cdot (T \to [x:T] \cdot P)$. So it is the case.

\

\noindent Case:

\

\infer{(T \to [\Gamma, x:T]T')(\Gamma T) \leadsto_\epsilon \Gamma T'}{}

\

\noindent We have $ \delta \cdot ((T \to [\Gamma,x:T]T')(\Gamma T)) \equiv (\delta T \to [\delta \Gamma, x:\delta T] \delta T') (\delta \Gamma \delta T) \leadsto_\epsilon \delta \Gamma \delta T' \equiv \delta \cdot (\Gamma T')$. 

\

\noindent Case:

\

\infer{\forall X.P \leadsto_\iota [T/X]\circ P}{}

\

\noindent We have $\forall X. \delta \cdot P \leadsto_\iota [T/X]\circ (\delta \cdot P) \equiv \delta \cdot ([T/X]\circ P)$. Assuming $[T/X]$ is capture avoiding w.r.t. $\delta$.

\

\noindent Case: 

\

\infer{P \leadsto_\pi \forall X.P}{}

\

\noindent $\delta \cdot P \leadsto_\pi \forall X. (\delta \cdot P) \equiv \delta \cdot (\forall X.P)$.

\

\noindent Case:

\

\infer{\Gamma x \leadsto_s \Gamma T}{(x:T) \in \Gamma}

\

\noindent $\delta\Gamma x \leadsto_s \delta \Gamma \delta T$, since $(x: \delta T) \in \delta \Gamma$.

\

\noindent Case:

\

\infer{\lambda x.P \leadsto \lambda x.P'}{P \leadsto P'}

\

\noindent By IH, we have $\delta \cdot P \leadsto \delta \cdot P'$. Thus we have $\lambda x.\delta \cdot P \equiv \delta \cdot (\lambda x.P) \leadsto \lambda x. \delta \cdot P'\equiv \delta \cdot (\lambda x.P')$.

\

\noindent Case: 

\

\infer{P_1 P_2 \leadsto P_1 P_2'}{P_2 \leadsto P_2' }

\

\noindent By IH,we have $\delta \cdot P_2 \leadsto \delta\cdot P_2'$. So $(\delta \cdot P_1) \delta\cdot P_2 \leadsto (\delta \cdot P_1) \delta \cdot P_2'$. So it is the case.

\

\noindent The other cases are similar.
\end{proof}


\begin{lemma}

\noindent If $P \leadsto P'$, then $[x:T]\cdot P \leadsto [x:T]\cdot P'$.

\end{lemma}

\begin{proof}
\noindent By induction on the derivation of $P \leadsto P'$.

\

\noindent Base Case 1: $\lambda x.P \leadsto_\lambda T_1 \to [x:T_1]\cdot P$. We also have
 $[y:T]\cdot (\lambda x.P) \equiv \lambda x.([y:T]\cdot P) \leadsto_\lambda T_1 \to [x:T_1] \cdot([y:T]\cdot P) \equiv [y:T]\cdot (T_1 \to [x:T_1]\cdot P)$. So it is
the case.

\

\noindent Base Case 2: $(T \to [\Gamma,y:T]T')\Gamma T \leadsto_\epsilon \Gamma T'$. We also have $[x:T''] \cdot
((T \to [\Gamma,y:T]T' )\Gamma T) \equiv (T \to [\Gamma , x:T'',y:T]T' )[\Gamma,x:T'']T \leadsto_\epsilon [\Gamma, y:T]T'$.

\

\noindent Base Case 3: $P \leadsto_\pi \forall X.P$. Then $[x:T]\cdot P \leadsto_\pi \forall X.[x:T]\cdot P \equiv [x:T]\cdot (\forall X.P)$.

\

\noindent Base Case 4: $\forall X.P \leadsto_\iota [U/X]\circ P$. Then $[x:T]\cdot(\forall X.P) \equiv \forall X.([x:T]\cdot P) \leadsto_\iota [U/X]\circ([x:T]\cdot P)\equiv [x:T] \cdot ([U/X]\circ P)$. 

\

\noindent Base Case 5: $\Gamma x \leadsto_s \Gamma T$, where $(x:T) \in \Gamma$.
It is the case.

\

\noindent Step Case: $P \equiv E[P_1] \leadsto P' \equiv  E[P_2]$, where $P_1 \leadsto P_2$. We need to show $[x:T]\cdot E[P_1] \leadsto [x:T]\cdot E[P_2]$. By case split on the form of $E$: 

\

\noindent If $E \equiv T \to E$. Then $[x:T]\cdot (T' \to P_1) \equiv T' \to [x:T]\cdot P_1$. By IH, we have $[x:T] \cdot P_1 \leadsto [x:T]\cdot P_2$.
Thus $T' \to [x:T]\cdot P_1 \leadsto T' \to [x:T]\cdot P_2$.

\

\noindent If $E \equiv E P''$. Then $[x:T]\cdot (P_1  P'') \equiv [x:T]\cdot P_1 ( [x:T]\cdot P'')$. By IH, we have $[x:T] \cdot P_1 \leadsto [x:T]\cdot P_2$.
Thus $[x:T]\cdot P_1 ([x:T]\cdot P'') \leadsto [x:T]\cdot P_2( [x:T]\cdot P'')$.

\

\noindent If $E \equiv  \forall X.E$. Then $[x:T]\cdot (\forall X.P_1) \equiv \forall X. ( [x:T]\cdot P_1)$. By IH, we have $[x:T] \cdot P_1 \leadsto [x:T]\cdot P_2$.
Thus $\forall X. ([x:T]\cdot P_1) \leadsto \forall X.( [x:T]\cdot P_2)$.

\

\noindent If $E \equiv \lambda y.E$. Then $[x:T]\cdot (\lambda y.P_1) \equiv \lambda y. ( [x:T]\cdot P_1)$. By IH, we have $[x:T] \cdot P_1 \leadsto [x:T]\cdot P_2$.
Thus $  \lambda y.([x:T]\cdot P_1) \leadsto \lambda y.([x:T]\cdot P_2)$.


\end{proof}


\begin{theorem}
\noindent If $\Gamma t \mulstep \Gamma T$, then $\Gamma \vdash t:T$. 

\end{theorem}

\begin{proof}
\noindent By induction on the structure of $t$.

\

\noindent Base Case: $t \equiv x$.

\

\noindent So we have $\Gamma x \mulstep \Gamma T$. It must be that $\Gamma x \mulstep_{\pi, \iota} \forall X^n.\Gamma x \leadsto_s \forall X^n.\Gamma T' \mulstep_{\pi, \iota} \Gamma T$, where $(x:T') \in \Gamma$. So by the restriction on $\leadsto_\pi$ and $\leadsto_\iota$, we have $\Gamma \vdash x:T$. 

\

\noindent Step Case: $t \equiv t_1 t_2$.

\

\noindent We have $(\Gamma t_1)(\Gamma t_2) \mulstep \Gamma T$. By lemma ~\ref{appin}, we have $(\Gamma t_1)(\Gamma t_2) \mulstep \forall Y^n.(T_1 \to [\Gamma,x:T_1]T_2)T_1 \leadsto_\epsilon
\forall Y^n.\Gamma T_2 \mulstep \Gamma T$, $\Gamma t_1 \mulstep T_1 \to [\Gamma, x:T_1]T_2$ and $ \Gamma t_2 \mulstep \Gamma T_1$. By IH, we have $\Gamma \vdash t_1:T_1 \to T_2$ and $\Gamma \vdash t_2 :T_1$. So we have $\Gamma \vdash t_1 t_2 : T_2$. 
Since $\forall Y^n.\Gamma T_2 \mulstep_{\pi,\iota} \Gamma T$, it must be the case that $\Gamma \vdash t_1 t_2: T$.

\

\noindent Step Case: $t \equiv \lambda x.t'$.

\

We have $\lambda x.(\Gamma t') \mulstep \Gamma T$. By lemma ~\ref{absin}, we have
$\lambda x.\Gamma t' \mulstep \forall Y^n.(\lambda x.P) \leadsto_\lambda \forall Y^n.(T_1 \to [x:T_1]\cdot P) \mulstep \Gamma T$ and $\Gamma t' \mulstep P$. We also have $[\Gamma,x:T_1]t' \mulstep [x:T_1]\cdot P$ by compatible with contextual action. By lemma ~\ref{arrow}, we have $T \equiv \forall Z^n.(T_3 \to T_4)$, $\delta T_1 \equiv T_3$ and $[x:\delta T_1]\cdot \delta P \mulstep [\Gamma,x:T_3]T_4 $. Since $dom(\delta) \cap FV(\Gamma) = \emptyset$, we have $\delta ([\Gamma,x:T_1]t') \equiv [\Gamma,x:\delta T_1]t'  \mulstep [x:\delta T_1]\cdot \delta P  \mulstep [\Gamma,x:T_3]T_4 $. Thus we have
 $[\Gamma, x: T_3]t' \mulstep [\Gamma,x:T_3]T_4$. By IH, we have $\Gamma,x:T_3 \vdash t': T_4$. Thus we have $\Gamma \vdash \lambda x.t':\forall Z^n.(T_3 \to T_4)$. 




\end{proof}

\end{document}
